package com.googlecode.kipler.satisfiability.completion.rule.formula.uniformnotation;

import com.googlecode.kipler.syntax.LTLBinaryOperator;
import com.googlecode.kipler.syntax.LTLUnaryOperator;
import com.googlecode.kipler.syntax.formula.BooleanFormula;
import com.googlecode.kipler.syntax.formula.Formula;
import com.googlecode.kipler.syntax.formula.LTLBinaryFormula;
import com.googlecode.kipler.syntax.formula.LTLUnaryFormula;


public class UntilBetaFormula implements BetaFormula {

	private LTLBinaryFormula binCon;

	private Formula beta1, beta2;

	private boolean valid;

	public UntilBetaFormula() {
		super();
	}

	public UntilBetaFormula(Formula Formula) {
		setBeta(Formula);
	}

	@Override
	public Formula getBeta() {
		return binCon;
	}

	@Override
	public void setBeta(Formula Formula) {
		valid = false;
		if (Formula instanceof LTLBinaryFormula) {
			binCon = (LTLBinaryFormula) Formula;
			if (binCon.getConstructor() == LTLBinaryOperator.UNTIL) {
				beta1 = binCon.getRhs();
				beta2 = new BooleanFormula(BooleanFormula.Operator.AND, binCon
						.getLhs(), new LTLUnaryFormula(LTLUnaryOperator.NEXT,
						binCon));
				valid = true;
			}
		}
	}

	@Override
	public Formula getBeta1() {
		return beta1;
	}

	@Override
	public Formula getBeta2() {
		return beta2;
	}

	public boolean isValid() {
		return valid;
	}

}
